Heavy duty set theory project

Goal

A set theory that can be used for axiomatizing AI and that is suitable
for interactive theorem proving, automatic theorem proving and use
in AI shells.

Requirements and specifications.

1. The theory is a notational extension of ZF, perhaps a mathematical
extension also.

2. Any deviation from the standard mathematical logic and set theory
conventions must be specifically justified.  There will be a lot.

3. The internal language is in the form of Lisp lists.

4. Lisp objects, e.g. S-expressions and Lisp functions, can be
members of sets.  This seems to require a set theory with ur-elements,
but perhaps it will be convenient to make a correspondence between
the Lisp entities and sets built from the null set.  If this is
done, however, representation of sets in memory and the printed
and input form of sets must be economical, readable and writable.

5. The treatment of functions with variable numbers of arguments
must be better than that of EKL - anyway no worse.  On second
thought, maybe the basic language should not have functions with
variable numbers of arguments, and this should be reserved for
a meta-level.  The metalanguage must then be well enough designed
so that metatheorems that allow for different numbers of arguments
can be stated and proved.